#ifndef __CDCL_DEPENDENCE_GRAPH__
#define __CDCL_DEPENDENCE_GRAPH__
#include "var.h"
#include "list.h" 
#include "common.h"
typedef enum Ltype {
    UNKNOWN, DECISION, STANDARD,
}Ltype;
typedef struct _literalset literal_set;
typedef struct _DGDecisionLiteral DGDecisionLiteral;
typedef struct _DGliteral{
    //Literal's type

    Ltype type;
    
    //the variable it self, copied to here
    __uint16_t varname;
    __uint16_t varsign;
    DGDecisionLiteral* implied_by;
    literal_set* parents;
    literal_set* children;
    literal_set* RESERVE;
} DGliteral;

struct _DGDecisionLiteral{
    DGliteral literal;
    literal_set* implies;
};

typedef struct _DGStandardLiteral{
    DGliteral literal;
} DGStandardLiteral;

struct _literalset{
    int *is_in_set;
    DGliteral** literals;
};
literal_set* new_literal_set();
DGliteral* new_literal(__uint16_t name, __uint16_t sign);
DGDecisionLiteral* new_decision_literal(__uint16_t name, __uint16_t sign);
DGStandardLiteral* new_standard_literal(DGliteral* p, __uint16_t name, __uint16_t sign);
void set_add_literal(literal_set* ls, DGliteral* l);
int set_num(literal_set* ls);
DGliteral* set_find(literal_set* ls, DGliteral* l);
DGliteral* set_get_first(literal_set* ls);
void Decision_add_imply(DGDecisionLiteral* l, DGliteral* imp);
void literal_add_child(DGliteral* l, DGliteral* child);
typedef struct _DGraph{
    _bool has_conflict;
    __uint16_t conflict;
    literal_set* lookup_map;
    literal_set* free;
}DGraph;
DGraph* new_graph();
void graph_add_node(DGraph* g, DGliteral*l);
DGliteral* graph_find(DGraph* g, const variable* v);
DGliteral* graph_find_negation(DGraph* g, const variable* v);
void remove_node(DGraph* graph, DGliteral* l);


// typedef struct _queuenode{
//     struct _queuenode* prev;
//     struct _queuenode* next;
//     void* data;
// }queuenode;

// typedef struct _queue{
//     struct _queuenode* first;
//     struct _queuenode* last;
// }queue;

// void init_queue(queue* q);
// void push_queue(queue* q, void* data);
// void* pop_queue(queue* q);
void print_graph(DGraph*g);
void show_graph_nodes(DGraph* g);
void literal_free(DGliteral* g, int decision);
void free_literal_set(literal_set* ls);

#endif